theory Design_InvokeCommand
imports "../DesignSpec"
begin

section "auxiliary function"

definition TA_InvokeCommandEntryPointR :: "Sys_Config ⇒ StateR 
    ⇒ COMMAND_ID_TYPE option ⇒ THREAD_ID_TYPE ⇒ StateR" where
          "TA_InvokeCommandEntryPointR sc s opt tid≡ 
              let s' = s⇓(TA_InvokeCommandEntryPoint sc (⇑s) opt tid) in
                        s'⦇IPC_driver:=IPC_driver s⦈"

definition tee_invokeTACommand_TEEDomain2R ::
  "Sys_Config ⇒ StateR ⇒ SESSION_ID_TYPE option ⇒ TIMEOUT_TYPE option ⇒ COMMAND_ID_TYPE option ⇒ PARAMS_TYPE option ⇒ PARAMS_TYPE option 
   ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEEC_RETURN_CODE_TYPE × PARAMS_TYPE option" where
  "tee_invokeTACommand_TEEDomain2R sc s ses_id time_out cmd_id in_params out_params ≡
    let 
      s' = (tee_invokeTACommand_TEEDomain2 sc (⇑s) ses_id time_out cmd_id in_params out_params)
    in
      (s⇓(fst s'),fst(snd s'),fst(snd(snd s')),snd(snd(snd s')))"

section "TEEC_InvokeCommand"

definition TEEC_InvokeCommand1R ::
  "Sys_Config ⇒ StateR ⇒ SESSION_ID_TYPE option ⇒ TIMEOUT_TYPE ⇒ COMMAND_ID_TYPE ⇒ PARAMS_TYPE ⇒ PARAMS_TYPE
  ⇒ (MemBlock × TEEC_MEMREF_TYPE) ⇒ StateR × TEEC_RET_ORIGIN × TEEC_RETURN_CODE_TYPE × PARAMS_TYPE" where
  "TEEC_InvokeCommand1R sc s ses_id time_out cmd_id in_params out_params memBlock_memRef ≡
    let
      s' = (TEEC_InvokeCommand1 sc (⇑s) ses_id time_out cmd_id in_params out_params memBlock_memRef)
    in
      (s⇓(fst s'), fst(snd s'), fst(snd(snd s')), snd(snd(snd s')))"

definition TEEC_InvokeCommand2R :: "Sys_Config ⇒ StateR 
  ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEEC_RETURN_CODE_TYPE × PARAMS_TYPE option" where
  "TEEC_InvokeCommand2R sc s ≡
   let
      exec = (exec_prime s);
      p = fst (hd exec);
      ses_id = param1 p;
      time_out = param2 p;
      cmd_id = param6 p;
      in_params = param7 p;
      out_params = param8 p;
      sesID = the ses_id;
      s_rev_event = s⦇exec_prime := tl exec⦈;
      s_invoke = tee_invokeTACommand_TEEDomain2R sc s_rev_event ses_id time_out cmd_id in_params out_params;
      s_state = fst s_invoke;
      s2 = Driver_Read s_state smc_ex_init_read zx_mgr;
      s_origin = fst(snd s_invoke);
      s_code = fst(snd (snd s_invoke));
      s_params = (snd (snd (snd s_invoke)))
   in
      if current s ≠ TEE sc then
         (s, TEE_ORIGIN_TEE, TEEC_ERROR_BAD_PARAMETERS, out_params)
      else if (exec_prime s) = [] then
         (s, TEE_ORIGIN_TEE, TEEC_ERROR_BAD_PARAMETERS, out_params)
      else if snd (hd (exec_prime s)) ≠ TEEC_IC2 then
         (s, TEE_ORIGIN_TEE, TEEC_ERROR_BAD_PARAMETERS, out_params)
      else
         (s2, s_origin, s_code, s_params)"


definition TEEC_InvokeCommand3R :: "Sys_Config ⇒ StateR
  ⇒ StateR × TEEC_RET_ORIGIN × TEEC_RETURN_CODE_TYPE × PARAMS_TYPE option" where
  "TEEC_InvokeCommand3R sc s ≡
      let
        exec = (exec_prime s);
        p = fst (hd exec);
        ses_id = param1 p;
        time_out = param2 p;
        cmd_id = param6 p;
        in_params = param7 p;
        out_params = param8 p;
        sesID = the ses_id;
        serverID = findSesServTid (⇑s) sesID;
        server_tid = the(findSesServTid (⇑s) sesID);
        curServTaState = (TAs_state (⇑s)) (the serverID);
        curServSessList = TA_sessions (the curServTaState);  
        isSessIdInSessList = isSessIdInTaInsSessList curServSessList sesID;
        s_rev_event = s⦇exec_prime := tl exec⦈;
        s_invoke = TA_InvokeCommandEntryPointR sc s_rev_event cmd_id server_tid;
        s_postOps = s_invoke⇓(TEE_MgrPostOps (⇑s_invoke) server_tid);
        post_param_ops = TEE_post_param_operation in_params;
        param_error = ⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None, param5 = None, 
              param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
              param10 = None, param11 = None, param12=Some TEEC_ERROR_BAD_PARAMETERS, param13=None⦈;
        s_error_ret = s_rev_event⇓(setCurDomainAndEvent (⇑s_rev_event) (TEE sc) (param_error, TEEC_IC4));
        param_success = ⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None, param5 = None, 
              param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
              param10 = None, param11 = None, param12=Some TEEC_SUCCESS, param13=None⦈;
        s_success_ret = s_postOps⇓(setCurDomainAndEvent (⇑s_postOps) (TEE sc) (param_success, TEEC_IC4))
        
      in
        if exec = [] ∨ ses_id = None then
          (s, TEEC_ORIGIN_TRUSTED_APP, TEEC_ERROR_BAD_PARAMETERS, out_params)
        else if serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ server_tid then
          (s, TEEC_ORIGIN_TRUSTED_APP, TEEC_ERROR_BAD_PARAMETERS, out_params)
        else if snd (hd (exec_prime s)) ≠ TEEC_IC3 then
          (s, TEEC_ORIGIN_TRUSTED_APP, TEEC_ERROR_BAD_PARAMETERS, out_params)
        else if ses_id = None ∨ cmd_id = None ∨ isSessIdInSessList ≠ True ∨ serverID = None then 
          (s_error_ret, TEEC_ORIGIN_TRUSTED_APP, TEEC_ERROR_BAD_PARAMETERS, out_params)
        else
          (s_success_ret, TEEC_ORIGIN_TRUSTED_APP,TEEC_SUCCESS, out_params)"

definition TEEC_InvokeCommand4R :: "Sys_Config ⇒ StateR 
  ⇒ StateR × TEEC_RET_ORIGIN × TEEC_RETURN_CODE_TYPE" where
  "TEEC_InvokeCommand4R sc s ≡ 
  let
      exec = (exec_prime s);
      p = fst (hd exec);
      ses_id = param1 p;
      time_out = param2 p;
      cmd_id = param6 p;
      in_params = param7 p;
      out_params = param8 p;
      teec_ret_code = param12 p;
      tee_ret_code = param13 p;
      s_rev_event = s⦇exec_prime := tl exec⦈;
      s_driver_success = fst(Driver_Write_smc s_rev_event zx_mgr ZX_OKr smc_ex_init2);
      param_call_closeSession = ⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = Some ⦇login=DTC_IDENTITY,id=Some 0⦈, 
          param5 = None, param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
          param10 = None, param11 = None, param12=teec_ret_code, param13=tee_ret_code⦈;
      s_call_closeSession = s_rev_event⇓(setCurDomainAndEvent (⇑s_rev_event) (TEE sc) (param_call_closeSession, TEEC_CS2));
      s_driver_error = fst(Driver_Write_smc s_call_closeSession zx_mgr ZX_ERR_INTERNALr smc_ex_init)
  in
    if (exec_prime s) =[] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC4 ∨ current s ≠ TEE sc then 
      (s, TEEC_ORIGIN_TEE, TEEC_ERROR_BAD_PARAMETERS)
    else if teec_ret_code ≠ (Some TEEC_SUCCESS) then 
      (s_driver_error, TEEC_ORIGIN_TRUSTED_APP, TEEC_ERROR_BUSY)
    else 
      (s_driver_success, TEEC_ORIGIN_TEE, TEEC_SUCCESS)
  "

section "TEE_InvokeTACommand"

definition TEE_InvokeTACommand1R :: "Sys_Config ⇒ StateR ⇒ (MemBlock × TEEC_MEMREF_TYPE)
  ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE × PARAMS_TYPE option" where
  "TEE_InvokeTACommand1R sc s memBlock_memRef ≡
    let 
      s' = (TEE_InvokeTACommand1 sc (⇑s) memBlock_memRef)
    in
      (s⇓(fst s'), fst(snd s'), fst(snd(snd s')), (snd(snd(snd s'))))
  "

definition TEE_InvokeTACommand2R :: "Sys_Config ⇒ StateR 
  ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE × PARAMS_TYPE option" where
  "TEE_InvokeTACommand2R sc s ≡
    let 
      s' = (TEE_InvokeTACommand2 sc (⇑s))
    in
      (s⇓(fst s'), fst(snd s'), fst(snd(snd s')), (snd(snd(snd s'))))
  "

definition TEE_InvokeTACommand3R :: "Sys_Config ⇒ StateR
  ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE × PARAMS_TYPE option" where
  "TEE_InvokeTACommand3R sc s ≡
      let
        exec = (exec_prime s);
        p = fst (hd exec);
        ses_id = param1 p;
        time_out = param2 p;
        cmd_id = param6 p;
        in_params = param7 p;
        out_params = param8 p;
        sesID = the ses_id;
        serverID = findSesServTid (⇑s) sesID;
        server_tid = the(findSesServTid (⇑s) sesID);
        curServTaState = (TAs_state (⇑s)) (the serverID);
        curServSessList = TA_sessions (the curServTaState);  
        isSessIdInSessList = isSessIdInTaInsSessList curServSessList sesID;
        s_rev_event = s⦇exec_prime := tl exec⦈;
        s_invoke = TA_InvokeCommandEntryPointR sc s_rev_event cmd_id server_tid;
        s_postOps = s_invoke⇓(TEE_MgrPostOps (⇑s_invoke) server_tid);
        post_param_ops = TEE_post_param_operation in_params;
        param_error = ⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None, param5 = None, 
              param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
              param10 = None, param11 = None, param12=None, param13=Some TEE_ERROR_BAD_PARAMETERS⦈;
        s_error_ret = s_rev_event⇓(setCurDomainAndEvent (⇑s_rev_event) (TEE sc) (param_error, TEE_IC4));
        param_success = ⦇param1 = ses_id, param2 = time_out, param3 = None, param4 = None, param5 = None, 
              param6 = cmd_id, param7 = in_params, param8 = out_params, param9 = None,
              param10 = None, param11 = None, param12=None, param13=Some TEE_SUCCESS⦈;
        s_success_ret = s_postOps⇓(setCurDomainAndEvent (⇑s_postOps) (TEE sc) (param_success, TEE_IC4))
      in
        if exec = [] ∨ ses_id = None then 
          (s, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS, out_params)
        else if serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ server_tid then
          (s, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS, out_params)
        else if snd (hd (exec_prime s)) ≠ TEE_IC3 then
          (s, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS, out_params)
        else if ses_id = None ∨ cmd_id = None ∨ isSessIdInSessList ≠ True ∨ serverID = None then 
          (s_error_ret, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS, out_params)
        else
          (s_success_ret, TEE_ORIGIN_TRUSTED_APP, TEE_SUCCESS, out_params)
  "

definition TEE_InvokeTACommand4R :: "Sys_Config ⇒ StateR
  ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE" where
  "TEE_InvokeTACommand4R sc s ≡ 
    let 
      s' = (TEE_InvokeTACommand4 sc (⇑s))
    in
      (s⇓(fst s'), fst(snd s'), (snd(snd s')))
  "

end